$\forall$${\it es}$:event\_system\{i:l\}, $e$:es{-}E(${\it es}$), $x$:Id, $T$:Type.
\\[0ex]es{-}dtype(${\it es}$; loc($e$); $x$; $T$)
\\[0ex]$\Rightarrow$ ($\forall$$t$:rationals. es{-}state{-}after{-}elapsed(${\it es}$; $e$; $t$)($x$) = es{-}after(${\it es}$; $x$; $e$) $\in$ $T$)